拡張 (集合)

一般に通用する用語でない点に注意

「拡張」は1.の言い回しを採用した

別表現

$ \lang\mathcal B\rang_X=\Set{B\in2^X|\exist B'\subseteq B:B'\in\mathcal B}

性質

$ \because\forall X,\mathcal F:

$ \varnothing\in\mathcal F

$ \iff\forall F\in2^X:\varnothing\subseteq F\land\varnothing\in\mathcal F

$ \iff\forall F\in2^X\exist F'\subseteq F:F'\in\mathcal F

$ \iff2^X\subseteq\lang\mathcal F\rang_X

$ \underline{\iff2^X=\lang\mathcal F\rang_X\quad}_\blacksquare

$ \because\forall X,\mathcal F:

$ \varnothing\in\mathcal F

$ \iff\varnothing\in2^X\land\varnothing\subseteq\varnothing\in\mathcal F

$ \iff\varnothing\in2^X\land\exist F'\subseteq\varnothing:F'\in\mathcal F

$ \underline{\iff\varnothing\in\lang\mathcal F\rang_X\quad}_\blacksquare

$ \forall X,\mathcal F,\mathcal G:\lang\mathcal F\cup\mathcal G\rang_X=\lang\mathcal F\rang_X\cup\lang\mathcal G\rang_X

$ \forall X,Y,\mathcal F:X\subseteq Y\lor\mathcal F\subseteq2^Y\implies\lang\lang\mathcal F\rang_Y\rang_X=\lang\mathcal F\rang_X

$ \because\forall X,\mathcal F:

$ \lang\lang\mathcal F\rang_X\rang_X=\Set{F\in2^X|\exist F'\subseteq F:F'\in\lang\mathcal F\rang_X}

$ =\Set{F\in2^X|\exist F'\subseteq F\exist F''\subseteq F'\in2^X:F''\in\mathcal F}

$ =\Set{F\in2^X|\exist F'\exist F''\subseteq F'\subseteq F:F''\in\mathcal F}

$ =\Set{F\in2^X|\exist F''\subseteq F:F''\in\mathcal F}

$ =\lang\mathcal F\rang_X

$ \lang\Set{A}\rang_X=\Set{F\in2^X|2^F\cap\Set{A}\neq\varnothing}

$ =\Set{F\in2^X|A\subseteq F}

$ \left.\lang\Set{A}\rang_X\right|_A=\set{F|\exist F':F=F'\cap A\land A\subseteq F'\subseteq X}

$ =\set{F|\exist F':F=F'\cap A=A\land F'\subseteq X}

$ =\Set{A}

$ \lang\Set{A}\rang_A=\Set{F\in2^A|2^F\cap\Set{A}\neq\varnothing}

$ =\Set{F\in2^A|A\subseteq F}

$ =\Set{A}

$ \left.\mathcal F\right|_A:=\set{F|\exist F'\in\mathcal F:F=F'\cap A}

汎用的に定義し直す

$ \left.\mathcal F\right|_{\cap A}:=\Set{F|\exist F'\in\mathcal F:F=F'\cap A}

$ \left.\mathcal F\right|_{\setminus A}:=\Set{F|\exist F'\in\mathcal F:F=F'\setminus A}

性質

$ \forall X\neq\varnothing\forall A\neq\varnothing\forall\mathcal B:\lang\mathcal B\rang_X\in\mathscr F_X\implies\lang\left.\mathcal B\right|_{\cap A}\rang_A\in\mathscr F_A

proof

$ B_1,B_2\in\left.\mathcal B\right|_{\cap A}

$ \iff\exist B_1',B_2'\in\mathcal B:

$ \begin{dcases}B_1=B_1'\cap A\\B_2=B_2'\cap A\end{dcases}

$ \implies\exist B_1',B_2'\in\mathcal B:B_1\cap B_2=(B_1'\cap B_2')\cap A

$ \implies\exist B_{12}\in\lang\mathcal B\rang_X:B_1\cap B_2=B_{12}\cap A

$ \iff\exist B'\exist B\subseteq B'\subseteq X:B_1\cap B_2=B'\cap A\land B\in\mathcal B

$ \implies\exist B'\exist B\in\mathcal B:B\cap A\subseteq B_1\cap B_2=B'\cap A\subseteq A

$ \implies\exist B\in\left.\mathcal B\right|_{\cap A}:B\subseteq B_1\cap B_2\subseteq A

$ \underline{\iff B_1\cap B_2\in\lang\left.\mathcal B\right|_{\cap A}\rang_A\quad}_\blacksquare

$ \forall X\neq\varnothing\forall A\forall\mathcal F\in\mathscr F_X:A\in\mathcal F\implies\left.\mathcal F\right|_{\cap A}\in\mathscr F_A

$ \because\forall X\neq\varnothing\forall\mathcal F\in\mathscr F_X:

$ A\in\mathcal F

$ \implies\begin{dcases}A\in\mathcal F\\\lang\left.\mathcal F\right|_{\cap A}\rang_A\in\mathscr F_A\end{dcases}

$ \because A\in\mathcal F\implies A\neq\varnothing

$ \implies\begin{dcases}\lang\left.\mathcal F\right|_{\cap A}\rang_A\in\mathscr F_A\\\forall F:\end{dcases}

$ F\in\lang\left.\mathcal F\right|_{\cap A}\rang_A

$ \iff\exist F'\subseteq F\subseteq A\exist F''\in\mathcal F:F'=F''\cap A

$ \iff\exist F'\subseteq F\subseteq A\exist F''\in\mathcal F:F'=F''\cap A\in\mathcal F

$ \implies F\subseteq A\land F\in\lang\mathcal F\rang_X

$ \subseteq\mathcal F

$ \implies F\in\mathcal F\land F=F\cap A

$ \iff F\in\left.\mathcal F\right|_{\cap A}

$ \underline{\implies\left.\mathcal F\right|_{\cap A}\in\mathscr F_A\quad}_\blacksquare

$ \forall X\forall A\in2^X\forall\mathcal F\in\mathscr F_X:A\notin\mathcal F\implies\mathcal F\subseteq\lang\left.\mathcal F\right|_{\setminus A}\rang_X\in\mathscr F_X

proof

$ A\notin\mathcal F

$ \implies\begin{dcases}\exist F:F\in\mathcal F\\A\notin\mathcal F\end{dcases}

$ \implies\exist F:F\setminus A\in\left.\mathcal F\right|_{\setminus A}

$ \underline{\implies\left.\mathcal F\right|_{\setminus A}\neq\varnothing\quad}_\blacksquare

$ A\notin\mathcal F

$ \implies(

$ \varnothing\in\left.\mathcal F\right|_{\setminus A}

$ \iff\exist F\in\mathcal F:\varnothing=F\setminus A

$ \iff\exist F\in\mathcal F:F\subseteq A

$ \iff A\in\lang\mathcal F\rang_X

$ \iff A\in\mathcal F

$ \implies\bot

$ )

$ \underline{\implies\varnothing\notin\left.\mathcal F\right|_{\setminus A}\quad}_\blacksquare

$ A\notin\mathcal F

$ \implies\forall F_1,F_2:

$ F_1,F_2\in\left.\mathcal F\right|_{\setminus A}

$ \iff\exist F_1',F_2'\in\mathcal F:\begin{dcases}F_1=F_1'\setminus A\\F_2=F_2'\setminus A\end{dcases}

$ \implies\exist F_1',F_2'\in\mathcal F:F_1\cap F_2=(F_1'\setminus A)\cap(F_2'\setminus A)

$ = (F_1'\cap F_2')\setminus A

$ \implies\exist F'\in\mathcal F:F_1\cap F_2=F'\setminus A

$ \iff F_1\cap F_2\in\left.\mathcal F\right|_{\setminus A}

$ \subseteq\lang\left.\mathcal F\right|_{\setminus A}\rang_X

$ \underline{\implies\forall F_1,F_2\in\left.\mathcal F\right|_{\setminus A}:F_1\cap F_2\in\lang\left.\mathcal F\right|_{\setminus A}\rang_X\quad}_\blacksquare

$ \forall X\forall F:

$ F\in\mathcal F\cap2^X

$ \iff F\setminus A\subseteq F\in\mathcal F\cap2^X

$ \implies\exist F'\in\left.\mathcal F\right|_{\setminus A}:F'\subseteq F\subseteq X

$ \iff F\in\lang\left.\mathcal F\right|_{\setminus A}\rang_X

$ \lang\Set{H|\exist F\in\mathcal F\exist G\in\mathcal G:H=F\cap G}\rang_X

$ = \Set{H\in2^X|\exist H'\subseteq H\exist F\in\mathcal F\exist G\in\mathcal G: H'= F\cap G}

$ = \Set{H\in2^X|\exist F\in\mathcal F\exist G\in\mathcal G:F\cap G\subseteq H}

$ =\left\lang\bigcup_{G\in\mathcal G}\left.\mathcal F\right|_{\cap G}\right\rang_X

(F3a)は

$ H_1,H_2\in\mathcal F\Cap\mathcal G

$ \iff\exist F_1,F_2\in\mathcal F\exist G_1,G_2\in\mathcal G:

$ \begin{dcases}H_1=F_1\cap G_1\\H_2=F_2\cap G_2\end{dcases}

$ \implies\exist F_1,F_2\in\mathcal F\exist G_1,G_2\in\mathcal G:H_1\cap H_2=(F_1\cap F_2)\cap(G_1\cap G_2)

$ \implies H_1\cap H_2\in\mathcal F\Cap\mathcal G

References